﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;

namespace AIproject
{
    class Clause : List<Literal>
    {
        private Model model;
        public string original_clause;
        public Clause(Model modelin)
        {
            model = modelin;
        }

        /// <summary>
        /// get a randomm symbol name
        /// </summary>
        /// <returns></returns>
        public string grab_random_symbol_name()
        {
            Random random = new Random();
            int index = random.Next(this.Count-1);
            return this[index].SymbolName;
        }

        /// <summary>
        /// evaluate the Clause
        /// </summary>
        /// <returns></returns>
        public bool evaluate()
        {
            foreach (Literal lit in this)
            {
                if (lit.evaluate())
                    return true;
            }
            return false;
        }

        /// <summary>
        /// see if a literal is in a clause
        /// </summary>
        /// <param name="l"></param>
        /// <param name="newClause"></param>
        /// <returns></returns>
        private bool is_literal_in_clause(Literal l, Clause newClause)
        {
                foreach(Literal l2 in newClause)
                {
                    if(l.isSame(l2))
                        return true;
                }
            return false;
        }


        /// <summary>
        /// Take two clauses and Union them
        /// </summary>
        /// <param name="c1"></param>
        /// <param name="c2"></param>
        /// <returns></returns>
        public Clause clauseUnion(Clause c1)
        {
            Clause newClause = new Clause(model);
            Clause concatClause = new Clause(model);
            if (this.Count == 0)
                return c1;
            if (c1.Count == 0)
                return this;
            concatClause = clone();
            //merge lists
            foreach (Literal lito in c1)
            {
               if(!concatClause.Contains(lito))
                concatClause.Add(lito);
            }

            foreach (Literal l in concatClause)
            {
                if (!is_literal_in_clause(l, newClause))
                    newClause.Add(l);
            }
            return newClause;


        }

        public bool is_same(Clause clause1)
        {
            if (this.Count() != clause1.Count())
                return false; //can not be the same
            for (int i=0; i < clause1.Count(); i++)
            {
                if (!this.contained_in(clause1[i]))//if one is in the other
                    return false; //not the same
            }
            return true; //is the same
        }

        public bool contained_in(Literal literal)
        {
            foreach (Literal l in this)
            {
                if (l.isSame(literal))
                    return true; //found it
            }
            return false;
            //throw new NotImplementedException();
        }

        /// <summary>
        /// remove a literal from the set
        /// </summary>
        /// <param name="l"></param>
        public void remove(Literal l)
        {
            for (int i = 0; i < this.Count; i++)
            {
                if (this[i].SymbolName == l.SymbolName && this[i].isNegation == l.isNegation)
                {
                    this.RemoveAt(i);
                    break;
                }
            }
        }

        /// <summary>
        /// clone the item
        /// </summary>
        /// <returns></returns>
        public Clause clone()
        {
            Clause newClause = new Clause(model);
            foreach (Literal l in this)
            {
                Literal lit = new Literal(model);
                lit.isNegation = l.isNegation;
                lit.SymbolName = l.SymbolName;
                newClause.Add(lit);
            }
            return newClause;
        }
    }
}
